$\forall$$E$:Type, $x_{1}$, $x_{2}$:$E$. tree\_leaf($x_{1}$) $=$ tree\_leaf($x_{2}$) $\in$ Tree($E$) $\Rightarrow$ $x_{1}$ $=$ $x_{2}$